package pl.edu.pw.elka.dzielins.revanalyzer.alloy.io;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileNotFoundException;
import java.io.FileOutputStream;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.OutputStream;
import java.nio.file.FileSystems;
import java.nio.file.Files;
import java.nio.file.LinkOption;
import java.nio.file.Path;
import java.nio.file.StandardCopyOption;
import java.util.ArrayList;
import java.util.HashSet;
import java.util.LinkedHashSet;
import java.util.List;
import java.util.Map;
import java.util.Set;

import org.apache.commons.lang3.StringUtils;
import org.apache.commons.math3.analysis.function.Log;
import org.apache.log4j.Logger;

import pl.edu.pw.elka.dzielins.revanalyzer.Project;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.Instance;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceObject;
import pl.edu.pw.elka.dzielins.revanalyzer.instance.InstanceRelation;
import pl.edu.pw.elka.dzielins.revanalyzer.model.Model;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelFact;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelObject;
import pl.edu.pw.elka.dzielins.revanalyzer.model.ModelRelation;

public class Writer {
	private static final Logger LOG = Logger.getLogger(Writer.class);
	
	public void writeAlloy(Instance instance, Model model, File file) throws Exception {
		BufferedWriter out = new BufferedWriter(new FileWriter(file, false));
		BufferedReader in = new BufferedReader(new FileReader("strippedModel"));
		String line;
		out.flush();
		// write stripped model
		while ((line = in.readLine()) != null) {
			out.write(line);
			out.newLine();
		}
		// write model facts
		for (ModelFact fact : model.getFacts()) {
			for (int i=0;i<fact.getDeclaration().length;++i) {
				out.write(fact.getDeclaration()[i]);
				out.newLine();
			}
		}
		in.close();
		out.newLine();
		// write instance
		out.write("// Signatures declarations");
		out.newLine();
		Map<ModelObject, Set<InstanceObject>> inheritanceMap = instance.getInheritanceMap();
		Map<ModelObject, Set<ModelObject>> hiearachyMap = model.getHiearchyMap();
		Set<String> set;
		// write InstanceObjects for each ModelObject
		for (ModelObject modelObject : inheritanceMap.keySet()) {
			out.write("// Instances of " + modelObject.getName());
			out.newLine();
			set = new LinkedHashSet<String>();
			// subsets
			for (ModelObject mo : hiearachyMap.get(modelObject))
				set.add(mo.getName());
			// atoms
			for (InstanceObject io : inheritanceMap.get(modelObject))
				set.add(io.getName());
			out.write("one sig " + StringUtils.join(set, ", ") + " extends " + modelObject.getName() + " {}");
			out.newLine();
			out.write("fact " + modelObject.getName() + "_Inheritance {");
			out.newLine();
			out.write(modelObject.getName() + " = "	+ StringUtils.join(set, " + "));
			out.newLine();
			out.write("}");
			out.newLine();
			out.newLine();
		}
		// write InstanceRelations for each InstanceObject
		for (InstanceObject instanceObject : instance.getObjects()) {
			if (instanceObject.getRelations().isEmpty() && instanceObject.getNotUsedRelations().isEmpty())
				continue;
			out.write("// Relations of " + instanceObject.getName());
			out.newLine();
			out.write("fact " + instanceObject.getName() + "_Assignments {");
			out.newLine();
			// write used relations
			for (ModelRelation mr : instanceObject.getRelations().keySet()) {
				if (instanceObject.getRelations().get(mr).isEmpty())
					continue;
				set = new HashSet<String>();
				out.write(instanceObject.getName() + "." + mr.getName()	+ " = ");
				for (InstanceRelation relation : instanceObject.getRelations().get(mr)) {
					if (relation.getBaseRelation().getArguments().size() == 1) {
						for (InstanceObject argument : relation.getArguments())
							set.add(argument.getName());
					} else {
						set.add("("+StringUtils.join(relation.getArgumentNames(), " -> ")+")");
					}
				}
				out.write(StringUtils.join(set, " + "));
				out.newLine();
			}
			// write not used relations
			for (ModelRelation mr : instanceObject.getNotUsedRelations()) {
				out.write("no " + instanceObject.getName() + "." + mr.getName());
				out.newLine();
			}
			out.write("}");
			out.newLine();
			out.newLine();
		}
		// write command
		out.write("run {} for 10 Int");
		for (ModelObject modelObject : model.getObjects()) {
			int count = 0;
			try {
				count = instance.getInheritanceMap().get(modelObject).size();
			} catch (NullPointerException e) {
				
			}
			out.write(", exactly " + String.valueOf(count) + " " + modelObject.getName());
		}
		out.newLine();
		out.close();
	}

}
